0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxTRS
↳3 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳10 CpxTypedWeightedCompleteTrs
↳11 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳12 CpxRNTS
↳13 InliningProof (UPPER BOUND(ID), 259 ms)
↳14 CpxRNTS
↳15 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CpxRNTS
↳17 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳18 CpxRNTS
↳19 IntTrsBoundProof (UPPER BOUND(ID), 300 ms)
↳20 CpxRNTS
↳21 IntTrsBoundProof (UPPER BOUND(ID), 10 ms)
↳22 CpxRNTS
↳23 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳24 CpxRNTS
↳25 IntTrsBoundProof (UPPER BOUND(ID), 156 ms)
↳26 CpxRNTS
↳27 IntTrsBoundProof (UPPER BOUND(ID), 7 ms)
↳28 CpxRNTS
↳29 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳30 CpxRNTS
↳31 IntTrsBoundProof (UPPER BOUND(ID), 163 ms)
↳32 CpxRNTS
↳33 IntTrsBoundProof (UPPER BOUND(ID), 37 ms)
↳34 CpxRNTS
↳35 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳36 CpxRNTS
↳37 IntTrsBoundProof (UPPER BOUND(ID), 114 ms)
↳38 CpxRNTS
↳39 IntTrsBoundProof (UPPER BOUND(ID), 6 ms)
↳40 CpxRNTS
↳41 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳42 CpxRNTS
↳43 IntTrsBoundProof (UPPER BOUND(ID), 162 ms)
↳44 CpxRNTS
↳45 IntTrsBoundProof (UPPER BOUND(ID), 26 ms)
↳46 CpxRNTS
↳47 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳48 CpxRNTS
↳49 IntTrsBoundProof (UPPER BOUND(ID), 114 ms)
↳50 CpxRNTS
↳51 IntTrsBoundProof (UPPER BOUND(ID), 53 ms)
↳52 CpxRNTS
↳53 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳54 CpxRNTS
↳55 IntTrsBoundProof (UPPER BOUND(ID), 97 ms)
↳56 CpxRNTS
↳57 IntTrsBoundProof (UPPER BOUND(ID), 15 ms)
↳58 CpxRNTS
↳59 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳60 CpxRNTS
↳61 IntTrsBoundProof (UPPER BOUND(ID), 155 ms)
↳62 CpxRNTS
↳63 IntTrsBoundProof (UPPER BOUND(ID), 3 ms)
↳64 CpxRNTS
↳65 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳66 CpxRNTS
↳67 IntTrsBoundProof (UPPER BOUND(ID), 3359 ms)
↳68 CpxRNTS
↳69 IntTrsBoundProof (UPPER BOUND(ID), 37 ms)
↳70 CpxRNTS
↳71 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳72 CpxRNTS
↳73 IntTrsBoundProof (UPPER BOUND(ID), 146 ms)
↳74 CpxRNTS
↳75 IntTrsBoundProof (UPPER BOUND(ID), 28 ms)
↳76 CpxRNTS
↳77 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳78 CpxRNTS
↳79 IntTrsBoundProof (UPPER BOUND(ID), 830 ms)
↳80 CpxRNTS
↳81 IntTrsBoundProof (UPPER BOUND(ID), 15 ms)
↳82 CpxRNTS
↳83 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳84 CpxRNTS
↳85 IntTrsBoundProof (UPPER BOUND(ID), 1395 ms)
↳86 CpxRNTS
↳87 IntTrsBoundProof (UPPER BOUND(ID), 48 ms)
↳88 CpxRNTS
↳89 FinalProof (⇔, 0 ms)
↳90 BOUNDS(1, n^1)
natsFrom(N) → cons(N, n__natsFrom(n__s(N)))
fst(pair(XS, YS)) → XS
snd(pair(XS, YS)) → YS
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → u(splitAt(N, activate(XS)), N, X, activate(XS))
u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS)
head(cons(N, XS)) → N
tail(cons(N, XS)) → activate(XS)
sel(N, XS) → head(afterNth(N, XS))
take(N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → snd(splitAt(N, XS))
natsFrom(X) → n__natsFrom(X)
s(X) → n__s(X)
activate(n__natsFrom(X)) → natsFrom(activate(X))
activate(n__s(X)) → s(activate(X))
activate(X) → X
natsFrom(N) → cons(N, n__natsFrom(n__s(N)))
splitAt(0, XS) → pair(nil, XS)
u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS)
head(cons(N, XS)) → N
activate(X) → X
snd(pair(XS, YS)) → YS
take(N, XS) → fst(splitAt(N, XS))
activate(n__s(X)) → s(activate(X))
afterNth(N, XS) → snd(splitAt(N, XS))
activate(n__natsFrom(X)) → natsFrom(activate(X))
s(X) → n__s(X)
fst(pair(XS, YS)) → XS
tail(cons(N, XS)) → activate(XS)
natsFrom(X) → n__natsFrom(X)
sel(N, XS) → head(afterNth(N, XS))
natsFrom(N) → cons(N, n__natsFrom(n__s(N))) [1]
splitAt(0, XS) → pair(nil, XS) [1]
u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS) [1]
head(cons(N, XS)) → N [1]
activate(X) → X [1]
snd(pair(XS, YS)) → YS [1]
take(N, XS) → fst(splitAt(N, XS)) [1]
activate(n__s(X)) → s(activate(X)) [1]
afterNth(N, XS) → snd(splitAt(N, XS)) [1]
activate(n__natsFrom(X)) → natsFrom(activate(X)) [1]
s(X) → n__s(X) [1]
fst(pair(XS, YS)) → XS [1]
tail(cons(N, XS)) → activate(XS) [1]
natsFrom(X) → n__natsFrom(X) [1]
sel(N, XS) → head(afterNth(N, XS)) [1]
natsFrom(N) → cons(N, n__natsFrom(n__s(N))) [1]
splitAt(0, XS) → pair(nil, XS) [1]
u(pair(YS, ZS), N, X, XS) → pair(cons(activate(X), YS), ZS) [1]
head(cons(N, XS)) → N [1]
activate(X) → X [1]
snd(pair(XS, YS)) → YS [1]
take(N, XS) → fst(splitAt(N, XS)) [1]
activate(n__s(X)) → s(activate(X)) [1]
afterNth(N, XS) → snd(splitAt(N, XS)) [1]
activate(n__natsFrom(X)) → natsFrom(activate(X)) [1]
s(X) → n__s(X) [1]
fst(pair(XS, YS)) → XS [1]
tail(cons(N, XS)) → activate(XS) [1]
natsFrom(X) → n__natsFrom(X) [1]
sel(N, XS) → head(afterNth(N, XS)) [1]
natsFrom :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil cons :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil n__natsFrom :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil n__s :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil splitAt :: 0 → n__s:n__natsFrom:cons:nil → pair 0 :: 0 pair :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil → pair nil :: n__s:n__natsFrom:cons:nil u :: pair → a → n__s:n__natsFrom:cons:nil → b → pair activate :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil head :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil snd :: pair → n__s:n__natsFrom:cons:nil take :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil fst :: pair → n__s:n__natsFrom:cons:nil s :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil afterNth :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil tail :: n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil sel :: 0 → n__s:n__natsFrom:cons:nil → n__s:n__natsFrom:cons:nil |
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
u
head
take
fst
tail
sel
splitAt
activate
afterNth
s
snd
natsFrom
snd(v0) → nil [0]
const, const1, const2
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
nil => 0
const => 0
const1 => 0
const2 => 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ s(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ s(s(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 2 }→ s(natsFrom(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ natsFrom(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(X1))) :|: X1 >= 0, z = 1 + (1 + X1)
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(X2))) :|: z = 1 + (1 + X2), X2 >= 0
afterNth(z, z') -{ 2 }→ snd(1 + 0 + XS) :|: z' = XS, z = 0, XS >= 0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
natsFrom(z) -{ 1 }→ 1 + N + (1 + (1 + N)) :|: z = N, N >= 0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sel(z, z') -{ 2 }→ head(snd(splitAt(N, XS))) :|: z' = XS, z = N, XS >= 0, N >= 0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
splitAt(z, z') -{ 1 }→ 1 + 0 + XS :|: z' = XS, z = 0, XS >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 2 }→ fst(1 + 0 + XS) :|: z' = XS, z = 0, XS >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(X) + YS) + ZS :|: z = 1 + YS + ZS, z'' = X, YS >= 0, X >= 0, z' = N, z1 = XS, ZS >= 0, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + N + (1 + (1 + N)) :|: z = N, N >= 0
natsFrom(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
splitAt(z, z') -{ 1 }→ 1 + 0 + XS :|: z' = XS, z = 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ s(s(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 2 }→ s(natsFrom(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(X1))) :|: X1 >= 0, z = 1 + (1 + X1)
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(X2))) :|: z = 1 + (1 + X2), X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z = 1 + X, X >= 0, X = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z' = XS, z = 0, XS >= 0, 1 + 0 + XS = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z' = XS, z = 0, XS >= 0, v0 >= 0, 1 + 0 + XS = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
natsFrom(z) -{ 1 }→ 1 + N + (1 + (1 + N)) :|: z = N, N >= 0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sel(z, z') -{ 4 }→ head(YS) :|: z' = XS, z = N, XS >= 0, N >= 0, XS = XS', N = 0, XS' >= 0, 1 + 0 + XS' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' = XS, z = N, XS >= 0, N >= 0, XS = XS', N = 0, XS' >= 0, v0 >= 0, 1 + 0 + XS' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
splitAt(z, z') -{ 1 }→ 1 + 0 + XS :|: z' = XS, z = 0, XS >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z' = XS, z = 0, XS >= 0, 1 + 0 + XS = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(X) + YS) + ZS :|: z = 1 + YS + ZS, z'' = X, YS >= 0, X >= 0, z' = N, z1 = XS, ZS >= 0, XS >= 0, N >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
{ natsFrom } { snd } { take } { fst } { splitAt } { s } { afterNth } { head } { activate } { sel } { tail } { u } |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: ?, size: O(n1) [3 + 2·z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: ?, size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: ?, size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: ?, size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: ?, size: O(n1) [1 + z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: ?, size: O(n1) [1 + z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: ?, size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: ?, size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 4 }→ head(YS) :|: z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 3 }→ head(0) :|: z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: ?, size: EXP |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ natsFrom(natsFrom(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 1 }→ activate(XS) :|: z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 1 }→ 1 + (1 + activate(z'') + YS) + ZS :|: z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP |
activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP |
activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: ?, size: O(n1) [z'] |
activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] |
activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] |
activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] tail: runtime: ?, size: INF |
activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] tail: runtime: O(n1) [4 + 4·z], size: INF |
activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] tail: runtime: O(n1) [4 + 4·z], size: INF |
activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] tail: runtime: O(n1) [4 + 4·z], size: INF u: runtime: ?, size: INF |
activate(z) -{ 3 + 4·z }→ s10 :|: s8 >= 0, s8 <= inf2, s9 >= 0, s9 <= 2 * s8 + 3, s10 >= 0, s10 <= 1 * s9 + 1, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s13 :|: s11 >= 0, s11 <= inf3, s12 >= 0, s12 <= 1 * s11 + 1, s13 >= 0, s13 <= 2 * s12 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s4 :|: s2 >= 0, s2 <= inf'', s3 >= 0, s3 <= 2 * s2 + 3, s4 >= 0, s4 <= 2 * s3 + 3, z - 2 >= 0
activate(z) -{ 3 + 4·z }→ s7 :|: s5 >= 0, s5 <= inf1, s6 >= 0, s6 <= 1 * s5 + 1, s7 >= 0, s7 <= 1 * s6 + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + N + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
afterNth(z, z') -{ 3 }→ YS :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
afterNth(z, z') -{ 2 }→ 0 :|: z = 0, z' >= 0, v0 >= 0, 1 + 0 + z' = v0
fst(z) -{ 1 }→ XS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
head(z) -{ 1 }→ N :|: z = 1 + N + XS, XS >= 0, N >= 0
natsFrom(z) -{ 1 }→ 1 + z :|: z >= 0
natsFrom(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 5 }→ s :|: s >= 0, s <= 1 * YS, z' >= 0, z >= 0, z = 0, 1 + 0 + z' = 1 + XS'' + YS, YS >= 0, XS'' >= 0
sel(z, z') -{ 4 }→ s' :|: s' >= 0, s' <= 1 * 0, z' >= 0, z >= 0, z = 0, v0 >= 0, 1 + 0 + z' = v0
snd(z) -{ 1 }→ YS :|: z = 1 + XS + YS, YS >= 0, XS >= 0
snd(z) -{ 0 }→ 0 :|: z >= 0
splitAt(z, z') -{ 1 }→ 1 + 0 + z' :|: z = 0, z' >= 0
tail(z) -{ 8 + 4·XS }→ s1 :|: s1 >= 0, s1 <= inf', z = 1 + N + XS, XS >= 0, N >= 0
take(z, z') -{ 3 }→ XS' :|: z = 0, z' >= 0, 1 + 0 + z' = 1 + XS' + YS, YS >= 0, XS' >= 0
u(z, z', z'', z1) -{ 8 + 4·z'' }→ 1 + (1 + s'' + YS) + ZS :|: s'' >= 0, s'' <= inf, z = 1 + YS + ZS, YS >= 0, z'' >= 0, ZS >= 0, z1 >= 0, z' >= 0
natsFrom: runtime: O(1) [1], size: O(n1) [3 + 2·z] snd: runtime: O(1) [1], size: O(n1) [z] take: runtime: O(1) [3], size: O(n1) [z'] fst: runtime: O(1) [1], size: O(n1) [z] splitAt: runtime: O(1) [1], size: O(n1) [1 + z'] s: runtime: O(1) [1], size: O(n1) [1 + z] afterNth: runtime: O(1) [5], size: O(n1) [z'] head: runtime: O(1) [1], size: O(n1) [z] activate: runtime: O(n1) [7 + 4·z], size: EXP sel: runtime: O(1) [9], size: O(n1) [z'] tail: runtime: O(n1) [4 + 4·z], size: INF u: runtime: O(n1) [8 + 4·z''], size: INF |